/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package chameleon.model.NuGatStructure.strategy;

import chameleon.model.NuGatStructure.symbTable.SymbLayer;
import chameleon.model.NuGatStructure.symbTable.SymbTable;
import chameleon.model.NuGatStructure.prop.PropGame;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.NuGatStructure.fsm.BddFsm;
import chameleon.model.NuGatStructure.fsm.GameBddFsm;
import chameleon.model.NuGatStructure.game.GamePlayer;
import chameleon.model.game.Game;
import chameleon.view.OutputManager;
import com.sun.jna.Pointer;

/**
 *
 * @author simon
 */
public abstract class GenBuchiStrategy extends GameStrategy {
    
    protected Node varList1_;
    protected Node varList2_;
    private SymbLayer layer_;
    protected boolean isSuccess_;
    
    //************************ CONSTRUCTOR *********************************//
    
    public GenBuchiStrategy(Pointer strategy,PropGame prop,Node varList1, 
            Node varList2, SymbLayer layer, NuGatInterface nugat){
        super (strategy,prop,nugat);
        varList1_ = varList1;
        varList2_ = varList2;
        layer_ = layer;
        this.setReverseInitialQuantifiers(0);
    }
    
    public GenBuchiStrategy (Pointer stragey, PropGame prop, SymbLayer layer,
            NuGatInterface nugat){
        super(stragey, prop, nugat);
        layer_ = layer;
    }
    
    @Override
    public abstract GenBuchiStrategy clone();
    
    //************************ DESTRUCTOR *********************************//
    
    public void destroy(SymbTable table){
        varList1_.freeNode();
        varList2_.freeNode();
        table.removeLayer(layer_);
        super.destroy();
    }
    
    //************************ SETTER ************************************//
    
    public final void setVarList1(Node varList1_) {
        this.varList1_ = varList1_;
    }

    public final void setVarList2(Node varList2_) {
        this.varList2_ = varList2_;
    }
    
    public void setIsSuccess(boolean isSuccess){
        isSuccess_ = isSuccess;
    }
    
    //************************ GETTER ************************************//
    public final boolean isSuccess(){
        return isSuccess_;
    }

    /**
     * This method takes a propGam that represent an ltl formula on format
     * 
     * (GFa && GFb && ...)
     * 
     * at the begining the structure of the node is
     * 
     * a && b && c && ...
     * 
     * and convert the proposition to an LTL formula.
     * @param prop
     * @return 
     */
    
    protected final Node getBuchiFormula (Node prop){
        Node ltlSpec;
        
        if (prop.car().notNull()){
            Node car = prop.car();
            
            ltlSpec = getGFFormula(car);
            
            prop = prop.cdr();
            if (prop.notNull()){
                while(prop.car().notNull()){
                    car = prop.car();
                    ltlSpec = new Node(nugat_.AND,getGFFormula(prop),ltlSpec,nugat_);
                    prop = prop.cdr();
                }
            }
        }
        else
            throw new RuntimeException("checkLtlSpec :: error the specification is empty");
        
        
        return ltlSpec;
    }
    
    /**
     * This function takes an atomic proposition and return
     * 
     * GF p
     * 
     * @param prop
     * @return 
     */
    
    private Node getGFFormula(Node prop){
        Node nullNode = new Node (Pointer.NULL,nugat_);
        Node eventually = new Node(nugat_.OP_FUTURE, prop,nullNode, nugat_);
        Node globally = new Node(nugat_.OP_GLOBAL , eventually, nullNode,nugat_);
        return globally;
    }
    
    protected SymbLayer getLayer(){
        return layer_;
    }
    
    //************************* PRINT ****************************************//
    
    public final void printStrategy(String file){
        checkStrategyExistence();
        GameStrategy strategy = this.clone();
        printStatus();
        
        int status;
        if (isSuccess())
            status = nugat_.GAME_REALIZABLE;
        else
            status = nugat_.GAME_UNREALIZABLE;            
            
        nugat_.Chameleon_Game_AfterCheckingSpec(prop_.ptr(),
                    status,
                    strategy.ptr(),
                    varList1_.ptr(),
                    varList2_.ptr(),
                    1, 0, 1, file);
    }
    
    @Override
    public final void printStatus(){
        super.printStatus();
        OutputManager output = new OutputManager();
        if (StrategyExists()){
            if (isSuccess())
                output.displayString(" : the strategy has been found\n");
            else
                output.displayString(" : no strategy exists\n");
        }
        else{
              output.displayString(" : no strategy exists\n");
        }
    }
    
    
    /**
     * This method check if the strategy present at the moment is winning. 
     * This strategy can be different than the original strategy provide by NuGaT.
     * Typically this strategy is a subset of the initial strategy. 
     * 
     * 
     * This checking is done by replay the game by fixing one player. This player
     * play the strategy.
     * @param game 
     */
    
    //@Override
    /*public void strategyIsWinning(Game game){
        GameBddFsm originalFsm = game.getGameBddFsm();
        GameBddFsm fsm ;
        boolean isSuccess;
        
        GamePlayer player = getPlayer();
        String strPlayer = player.toString();
        
        BddFsm playerBddFsm;
        BddFsm stratBddFsm;
        
        if (strPlayer.equals(nugat_.PLAYER_NAME_1)){
            playerBddFsm = game.getBddFsmP1().clone();
        }
        else{
            playerBddFsm = game.getBddFsmP2().clone();
        }
        
        
        //create the strategy bdd fsm
        stratBddFsm = getBddFsm(playerBddFsm, game.getOptsHandlerInstance(),
                game.getGlobalFsmBuilder());
        
        //Replace the transition relation for the player in the game fsm
        if (strPlayer.equals(nugat_.PLAYER_NAME_1))
            fsm = originalFsm.changePLayer1(stratBddFsm);
        else
            fsm = originalFsm.changePLayer2(stratBddFsm);
        
        isSuccess = getSuccess(player, fsm) ;
        
        OutputManager output = new OutputManager();
        if (isSuccess)
            output.displayString("The strategy is winning\n");
        else
            output.displayString("The strategy is not winning\n");
        
    }*/
    
    public abstract boolean getSuccess(GamePlayer player, GameBddFsm fsm);
    
}
